package org.xteam.sled.matcher;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Set;

import org.xteam.parser.runtime.Span;
import org.xteam.sled.ast.AbstractPattern;
import org.xteam.sled.ast.Equation;
import org.xteam.sled.model.AbsoluteDisjunct;
import org.xteam.sled.model.AbsoluteField;
import org.xteam.sled.model.AbsolutePattern;
import org.xteam.sled.model.AbsoluteProtoDisjunct;
import org.xteam.sled.model.AbsoluteProtoPattern;
import org.xteam.sled.model.AbsoluteSequence;
import org.xteam.sled.model.LabelledPattern;
import org.xteam.sled.model.PatternUtils;
import org.xteam.sled.model.RangeConstraint;
import org.xteam.sled.semantic.BooleanSemantic;
import org.xteam.sled.semantic.ForwardingEvaluationContext;
import org.xteam.sled.semantic.IDenotable;
import org.xteam.sled.semantic.IErrorContext;
import org.xteam.sled.semantic.IEvaluationContext;
import org.xteam.sled.semantic.PatternSemantic;
import org.xteam.sled.semantic.Range;
import org.xteam.sled.semantic.SemanticContext;
import org.xteam.sled.semantic.SolverContext;
import org.xteam.sled.semantic.Temporary;
import org.xteam.sled.semantic.exp.Exp;
import org.xteam.sled.semantic.exp.ExpAField;
import org.xteam.sled.semantic.exp.ExpCondition;
import org.xteam.sled.semantic.exp.ExpConst;
import org.xteam.sled.semantic.exp.ExpForce;
import org.xteam.sled.semantic.exp.ExpRewriter;
import org.xteam.sled.semantic.exp.ExpVar;
import org.xteam.sled.semantic.exp.FreeVariableCollector;
import org.xteam.sled.semantic.exp.VariableSubstitute;
import org.xteam.sled.solver.EquationSolver;
import org.xteam.sled.solver.SolverResult;

public class ArmBuilder {
	private AbstractPattern patternExpr;
	private List<Equation> equations = new ArrayList<Equation>();
	private String name;
	private Object code;

	private LabelledPattern pattern;
	private int uid;
	private Map<String, Exp> answers = new HashMap<String, Exp>();
	private Set<ExpCondition> conditions = new HashSet<ExpCondition>();
	private int patlen;
	
	public ArmBuilder(AbstractPattern pat, List<Equation> equations, String name,
			Object code) {
		this.patternExpr = pat;
		this.equations = equations;
		this.name = name;
		this.code = code;
	}

	public List<Arm> elaborate(SemanticContext ctxt, int i, String successor) {
		List<ExpCondition> eqns = new ArrayList<ExpCondition>();
		BooleanSemantic b = new BooleanSemantic(new SolverContext(ctxt));
		for (Equation equation : equations) {
			equation.visit(b);
			eqns.add(b.getExpression());
		}
		PatternSemantic p = new PatternSemantic(new MatcherContext(ctxt));
		patternExpr.visit(p);
		pattern = p.getPattern();
		pattern = pattern.actualizeLatents(/* actualsOk = */ true);
		return doPattern(eqns, successor);
	}
	
	private List<Arm> doPattern(List<ExpCondition> eqns, String successor) {
		AbsoluteProtoPattern p = pattern.anf();
		List<AbsoluteProtoDisjunct> dps = new ArrayList<AbsoluteProtoDisjunct>();
		for (AbsoluteProtoDisjunct apd : p.getDisjuncts()) {
			dps.add(moveConstantBindingsToConstraints(apd));
		}
		List<Map<String, Integer>> r = new ArrayList<Map<String, Integer>>();
		for (AbsoluteProtoDisjunct apd : dps) {
			r.add(labelOffsets(apd));
		}
		Set<String> allLabels = intersectIds (new MapSource(r));
		Set<String> allFree = intersectIds (new PatternSource(dps));
		//allFree.remove(wild);
		return splitArm(dps, allLabels, allFree, eqns, successor);
		
	}
	
	private List<Arm> splitArm(List<AbsoluteProtoDisjunct> dps, Set<String> allLabels, Set<String> allFree, List<ExpCondition> eqns, String successor) {
		int acount = 0;
		ArmResult lasta = null;
		List<Arm> res = new ArrayList<Arm>();
		for (AbsoluteProtoDisjunct d : dps) {
			FieldBindingResult r /*(s as (soln, conds), dd)*/ = fieldbindingsToSoln(d, allLabels, allLabels, allFree, eqns);
			Integer patlen = null;
			if (successor != null)
				patlen = d.getSequence().bitLength();
			if (lasta == null) {
				lasta = new ArmResult(r.disjuncts, patlen, r.result, r.conditions);
			} else {
				if (patlen == lasta.patlen
						&& lasta.disjuncts.get(0).getSequence().getLabels().equals(d.getSequence().getLabels())
						&& lasta.soln.equals(r.result)
						&& lasta.conditions.equals(r.conditions)) {
					lasta.addDisjuncts(r.disjuncts);
				} else {
					throw new RuntimeException("not completed");
				}
			}
		}
		if (lasta != null) {
			res.add(mkArm(lasta));
		}
		return res;
	}
	
	private static class ArmResult {

		private List<AbsoluteProtoDisjunct> disjuncts;
		private Integer patlen;
		private Map<String, Exp> soln;
		private List<Exp> conditions;

		public ArmResult(List<AbsoluteProtoDisjunct> disjuncts, Integer patlen,
				Map<String, Exp> soln, List<Exp> conditions) {
			this.disjuncts = disjuncts;
			this.patlen = patlen;
			this.soln = soln;
			this.conditions = conditions;
		}

		public void addDisjuncts(List<AbsoluteProtoDisjunct> dd) {
			disjuncts.addAll(dd);
		}
		
	}

	private Arm mkArm(ArmResult ar) {
		List<AbsoluteDisjunct> ads = new ArrayList<AbsoluteDisjunct>();
		for (AbsoluteProtoDisjunct apd : ar.disjuncts) {
			ads.add(new AbsoluteDisjunct(apd.name(), apd.getConditions(), apd.getSequence()));
		}
		return new Arm(new AbsolutePattern(pattern.name(), ads), ar.soln, ar.conditions);
	}

	private FieldBindingResult fieldbindingsToSoln(AbsoluteProtoDisjunct d,
			Set<String> inputs, Set<String> allLabels, Set<String> allFree, List<ExpCondition> eqns) {
		inputs = new HashSet<String>(inputs);
		inputs.addAll(d.getSequence().getLabels().keySet());
		eqns = new ArrayList<ExpCondition>(eqns);
		VarState varstate = new VarState();
		for (AbsoluteField f : d.getFieldBindings().keySet()) {
			String v = varstate.varFor(f);
			eqns.add(new ExpCondition(ExpCondition.EQ, d.getFieldBindings().get(f), new ExpVar(v)));
			inputs.add(v);
		}
		for (Exp e : d.getConditions()) {
			eqns.add((ExpCondition)e);
		}
		for (int i = 0; i < eqns.size(); ++i) {
			eqns.set(i, (ExpCondition)(new ExpRewriter() {
				public void visitForce(ExpForce e) {
					e.getExpr().visit(this);
				}
			}).rewrite(eqns.get(i)));
		}
		EquationSolver solver = new EquationSolver();
		SolverResult solveResult = solver.solve(inputs, eqns);
		if (solveResult.hasUnsolvables()) {
			solveResult = solver.solve(inputs, eqns, true);
			throw new RuntimeException("unsolvable equations " + solveResult.getUnsolvables());
		}
		Map<String, Exp> result = new HashMap<String, Exp>();
		for (String l : d.getSequence().getLabels().keySet()) {
			if (allLabels.contains(l)) {
				result.put(l, PatternUtils.addBitsToPC(d.getSequence().getLabels().get(l)));
			}
		}
		for (String l : allFree) {
			Map<String, Exp> values = solveResult.getValues();
			Exp e = values.get(l);
			if (e == null)
				e = new ExpVar("could not solve for " + l);
			result.put(l, new ConvertSubst(varstate).rewrite(e).superSymplify());
		}
		List<Exp> constraints = new ArrayList<Exp>();
		for (ExpCondition c : solveResult.getConstraints()) {
			constraints.add(new ConvertSubst(varstate).rewrite(
					new VariableSubstitute(solveResult.getValues()).rewrite(c)));
		}
		AbsoluteProtoPattern p = inequalitiesToPat(d.getSequence().bitLength(), constraints,
				new AbsoluteProtoPattern(new AbsoluteProtoDisjunct(d.name(), new HashSet<Exp>(), d.getSequence())));
		return new FieldBindingResult(result, p.getDisjuncts(), constraints);
	}
	
	private static class FieldBindingResult {

		private Map<String, Exp> result;
		private List<AbsoluteProtoDisjunct> disjuncts;
		private List<Exp> conditions;

		public FieldBindingResult(Map<String, Exp> result,
				List<AbsoluteProtoDisjunct> disjuncts,
				List<Exp> constraints) {
			this.result = result;
			this.disjuncts = disjuncts;
			this.conditions = constraints;
		}
		
	}
	
	private AbsoluteProtoPattern inequalitiesToPat(int len, List<Exp> constraints,
			AbsoluteProtoPattern absoluteProtoPattern) {
		Iterator<Exp> i = constraints.iterator();
		while (i.hasNext()) {
			Exp c = i.next();
			if (c instanceof ExpCondition) {
				if (((ExpCondition)c).left() instanceof ExpAField
						&& ((ExpCondition)c).right() instanceof ExpConst) {
					i.remove();
					AbsoluteField aField = ((ExpAField)((ExpCondition)c).left()).field();
					int relop = ((ExpCondition)c).condition();
					int offset = ((ExpConst)((ExpCondition)c).right()).value();
					absoluteProtoPattern = (AbsoluteProtoPattern) absoluteProtoPattern.and(
							AbsoluteProtoPattern.constraint(new NullErrorContext(), null,
									len, aField, relop, offset));
				} else if (((ExpCondition)c).left() instanceof ExpConst
						&& ((ExpCondition)c).right() instanceof ExpAField) {
					i.remove();
					AbsoluteField aField = ((ExpAField)((ExpCondition)c).right()).field();
					int relop = ExpCondition.reverseOp(((ExpCondition)c).condition());
					int offset = ((ExpConst)((ExpCondition)c).left()).value();
					absoluteProtoPattern = (AbsoluteProtoPattern) absoluteProtoPattern.and(
							AbsoluteProtoPattern.constraint(new NullErrorContext(), null,
									len, aField, relop, offset));
				}
			}
		}
		return absoluteProtoPattern;
	}
	
	private static class NullErrorContext implements IErrorContext {

		@Override
		public void reportError(Span span, String msg) {
		}
		
	}

	private static class ConvertSubst extends ExpRewriter {
		
		private VarState state;
		
		public ConvertSubst(VarState varstate) {
			this.state = varstate;
		}

		public void visitVar(ExpVar expVar) {
			AbsoluteField f = state.fieldFor(expVar.name());
			if (f != null) {
				stack.push(new ExpAField(f));
			} else {
				stack.push(expVar);
			}
		}
	}
	
	private static interface ISymbolSource {
		int length();
		Set<String> getSymbols(int i);
	}
	
	private static class MapSource implements ISymbolSource {

		private List<Map<String, Integer>> elements;

		public MapSource(List<Map<String, Integer>> elements) {
			this.elements = elements;
		}

		@Override
		public Set<String> getSymbols(int i) {
			return new HashSet<String>(elements.get(i).keySet());
		}

		@Override
		public int length() {
			return elements.size();
		}
		
	}
	
	private static class PatternSource implements ISymbolSource {

		private List<AbsoluteProtoDisjunct> elements;

		public PatternSource(List<AbsoluteProtoDisjunct> elements) {
			this.elements = elements;
		}

		@Override
		public Set<String> getSymbols(int i) {
			Set<String> res = new HashSet<String>();
			Map<AbsoluteField, Exp> bbs = elements.get(i).getFieldBindings();
			for (Exp e : bbs.values()) {
				res.addAll(FreeVariableCollector.get(e));
			}
			return res;
		}

		@Override
		public int length() {
			return elements.size();
		}
		
	}
	
	private Set<String> intersectIds(ISymbolSource source) {
		Set<String> res = new HashSet<String>();
		Set<String> w = new HashSet<String>();
		for (int i = 0; i < source.length(); ++i) {
			Set<String> current = source.getSymbols(0);
			if (i == 0) {
				res = current;
			} else {
				Set<String> inter = source.getSymbols(0);
				for (String name : current) {
					if (res.contains(name)) {
						inter.add(name);
					} else {
						w.add(name);
					}
				}
				current.removeAll(res);
				w.addAll(current);
				res = inter;
			}
		}
		return res;
	}

	private Map<String, Integer> labelOffsets(AbsoluteProtoDisjunct apd) {
		return apd.getSequence().getLabels();
	}

	private AbsoluteProtoDisjunct moveConstantBindingsToConstraints(AbsoluteProtoDisjunct apd) {
		Map<AbsoluteField, Exp> nbbs = new HashMap<AbsoluteField, Exp>();
		List<RangeConstraint<AbsoluteField>> nccs = new ArrayList<RangeConstraint<AbsoluteField>>();
		nccs.addAll(apd.getSequence().getConstraints());
		for (AbsoluteField bb : apd.getFieldBindings().keySet()) {
			Integer n = apd.getFieldBindings().get(bb).superSymplify().unConst();
			if (n == null) {
				nbbs.put(bb, apd.getFieldBindings().get(bb));
			} else {
				nccs.add(new RangeConstraint<AbsoluteField>(bb, new Range(n)));
			}
		}
		return new AbsoluteProtoDisjunct(apd.name(), apd.getConditions(),
				new AbsoluteSequence(nccs, apd.getSequence().getLabels(), apd.getSequence().bitLength()), nbbs);
	}
	
	private static class MatcherContext extends ForwardingEvaluationContext {

		public MatcherContext(IEvaluationContext context) {
			super(context);
		}
		
		public IDenotable lookup(String name, Span span) {
			IDenotable res = lookupOpt(name);
			if (res == null) {
				res = new Temporary(new ExpVar(name), null);
			}
			return res;
		}
		
	}
	
}
